D1, D2:dsys{i:l}. d-sub{i:l}(D1; D2)  {i'} 

latex

Definitions	x:A. B(x), Dsys, t  T, , D1  D2
Lemmas	Id wf, ma-sub wf, d-m wf, msga wf